#ifndef SAT_PARSE_H
#define SAT_PARSE_H 

#include "../cnf2aig/cnfToAig.h"
#include "ParseUtils.h"

using QuteRSAT::AigIndex;
using QuteRSAT::AigCircuit;
using QuteRSAT::CnfToAig;

template<class B, class Solver>
static void readClause(B& in, Solver& S, vector<uint32_t>& lits) {
    int     parsed_lit, var;
    lits.clear();
    for (;;){
        parsed_lit = parseInt(in);
        if (parsed_lit == 0) break;
        var = abs(parsed_lit);
        lits.push_back( var << 1 | (parsed_lit > 0) );
    }
}

template<class B>
static unsigned parse_header( B & in)
{
   int vars    = 0;
   int clauses = 0;
   for (;;){
       skipWhitespace(in);
       if (*in == 'p'){
          if (eagerMatch(in, "p cnf")){
             vars    = parseInt(in);
             clauses = parseInt(in);
             break;
          }
          else{
             printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
          }
       }
       else if (*in == 'c' || *in == 'p')
          skipLine(in);
   }
   return vars;
}

template<class B, class Solver>
static void parse_DIMACS(B& in, Solver& S) {
    vector<uint32_t> lits;
    int cnt     = 0;
    for (;;){
        skipWhitespace(in);
        if (*in == EOF) break;
        else if (*in == 'c' || *in == 'p')
            skipLine(in);
        else{
            cnt++;
            readClause(in, S, lits);
            S.addClause(lits); }
    }
}
#endif
